nLab set-theoretic multiverse

Redirected from "gros topos".
The set-theoretic multiverse

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

The set-theoretic multiverse

Idea

The set-theoretic multiverse is a philosophical perspective on set theory, advocated by Joel David Hamkins, according to which

there are many distinct concepts of set, each instantiated in a corresponding set-theoretic universe.

This is in contrast to the “universe view”, which

asserts that there is an absolute background set concept, with a corresponding absolute set-theoretic universe in which every set-theoretic question has a definite answer.

The set-theoretic multiverse is at least informally analogous to such categorical notions as Topos, the 2-category of toposes, with each topos regarded as a universe of (“variable”) sets. See at topos theory and at categorical logic for more on this.

In dependent type theory

In dependent type theory, the set-theoretic multiverse is given by the existence of multiple inequivalent models of set theory as types VV with well-founded relations \in, which are made into Tarski universes via the dependent sum type:

x:VEl(x) y:Vyxx:V \vdash \mathrm{El}(x) \coloneqq \sum_{y:V} y \in x

In addition, this extends to any other notion of set theory, such as the categorical models of set theory as well-pointed categories \mathcal{E}, which are made into Tarski universes by the hom-set

x:VEl(x)hom(1,x)x:V \vdash \mathrm{El}(x) \coloneqq \mathrm{hom}(1, x)

where 1:1:\mathcal{E} is the terminal separator of the category \mathcal{E}.

This all coexists with the usual type theoretic notion of universes of sets as Tarski universes UU with universal type family TT in which for every type A:UA:U in the universe, T(A)T(A) satisfies UIP.

References

Last revised on July 27, 2024 at 17:45:27. See the history of this page for a list of all contributions to it.